YES 2.488 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule List
  ((elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int) :: Eq a => a  ->  [a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Lambda Reductions:
The following Lambda expression
\vv1→
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR

mainModule List
  ((elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int) :: Eq a => a  ->  [a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR

mainModule List
  ((elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int) :: Eq a => a  ->  [a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) =  if p x then i : [] else []
findIndices00 p _ = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR

mainModule List
  ((elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int) :: Eq a => a  ->  [a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p _ = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR

mainModule List
  ((elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int) :: Eq a => a  ->  [a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int) :: Eq a => a  ->  [a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow

mainModule List
  (elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yv1000), Succ(yv11000)) → new_primEqNat(yv1000, yv11000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv5200), Succ(yv1101000)) → new_primPlusNat(yv5200, yv1101000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv10100), Succ(yv110100)) → new_primMulNat(yv10100, Succ(yv110100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(Left(yv100), Left(yv1100), app(ty_Maybe, eg), eh) → new_esEs(yv100, yv1100, eg)
new_esEs3(:(yv100, yv101), :(yv1100, yv1101), app(app(ty_Either, bdf), bdg)) → new_esEs1(yv100, yv1100, bdf, bdg)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), app(app(app(ty_@3, ec), ed), ee), df) → new_esEs2(yv100, yv1100, ec, ed, ee)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, he, app(app(ty_Either, baa), bab)) → new_esEs1(yv102, yv1102, baa, bab)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), app(app(app(ty_@3, bcf), bcg), bch), he, bah) → new_esEs2(yv100, yv1100, bcf, bcg, bch)
new_esEs3(:(yv100, yv101), :(yv1100, yv1101), app(app(ty_@2, bdd), bde)) → new_esEs0(yv100, yv1100, bdd, bde)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, app(app(ty_@2, bba), bbb), bah) → new_esEs0(yv101, yv1101, bba, bbb)
new_esEs(Just(yv100), Just(yv1100), app(app(ty_Either, bd), be)) → new_esEs1(yv100, yv1100, bd, be)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), cb, app(app(app(ty_@3, da), db), dc)) → new_esEs2(yv101, yv1101, da, db, dc)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, he, app(app(ty_@2, hg), hh)) → new_esEs0(yv102, yv1102, hg, hh)
new_esEs1(Left(yv100), Left(yv1100), app(ty_[], ga), eh) → new_esEs3(yv100, yv1100, ga)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, app(ty_[], bbh), bah) → new_esEs3(yv101, yv1101, bbh)
new_esEs3(:(yv100, yv101), :(yv1100, yv1101), app(ty_[], bec)) → new_esEs3(yv100, yv1100, bec)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, app(ty_Maybe, bag), bah) → new_esEs(yv101, yv1101, bag)
new_esEs(Just(yv100), Just(yv1100), app(ty_[], ca)) → new_esEs3(yv100, yv1100, ca)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), app(app(ty_@2, bcb), bcc), he, bah) → new_esEs0(yv100, yv1100, bcb, bcc)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, he, app(ty_Maybe, hf)) → new_esEs(yv102, yv1102, hf)
new_esEs1(Left(yv100), Left(yv1100), app(app(ty_Either, fc), fd), eh) → new_esEs1(yv100, yv1100, fc, fd)
new_esEs(Just(yv100), Just(yv1100), app(app(app(ty_@3, bf), bg), bh)) → new_esEs2(yv100, yv1100, bf, bg, bh)
new_esEs(Just(yv100), Just(yv1100), app(ty_Maybe, ba)) → new_esEs(yv100, yv1100, ba)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), cb, app(ty_[], dd)) → new_esEs3(yv101, yv1101, dd)
new_esEs1(Right(yv100), Right(yv1100), gb, app(app(ty_Either, gf), gg)) → new_esEs1(yv100, yv1100, gf, gg)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), app(ty_[], ef), df) → new_esEs3(yv100, yv1100, ef)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), app(app(ty_Either, ea), eb), df) → new_esEs1(yv100, yv1100, ea, eb)
new_esEs3(:(yv100, yv101), :(yv1100, yv1101), bdb) → new_esEs3(yv101, yv1101, bdb)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), app(ty_Maybe, bca), he, bah) → new_esEs(yv100, yv1100, bca)
new_esEs(Just(yv100), Just(yv1100), app(app(ty_@2, bb), bc)) → new_esEs0(yv100, yv1100, bb, bc)
new_esEs1(Left(yv100), Left(yv1100), app(app(ty_@2, fa), fb), eh) → new_esEs0(yv100, yv1100, fa, fb)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, app(app(ty_Either, bbc), bbd), bah) → new_esEs1(yv101, yv1101, bbc, bbd)
new_esEs1(Left(yv100), Left(yv1100), app(app(app(ty_@3, ff), fg), fh), eh) → new_esEs2(yv100, yv1100, ff, fg, fh)
new_esEs1(Right(yv100), Right(yv1100), gb, app(app(app(ty_@3, gh), ha), hb)) → new_esEs2(yv100, yv1100, gh, ha, hb)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, he, app(ty_[], baf)) → new_esEs3(yv102, yv1102, baf)
new_esEs3(:(yv100, yv101), :(yv1100, yv1101), app(app(app(ty_@3, bdh), bea), beb)) → new_esEs2(yv100, yv1100, bdh, bea, beb)
new_esEs1(Right(yv100), Right(yv1100), gb, app(ty_[], hc)) → new_esEs3(yv100, yv1100, hc)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, app(app(app(ty_@3, bbe), bbf), bbg), bah) → new_esEs2(yv101, yv1101, bbe, bbf, bbg)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), app(ty_Maybe, de), df) → new_esEs(yv100, yv1100, de)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), app(ty_[], bda), he, bah) → new_esEs3(yv100, yv1100, bda)
new_esEs1(Right(yv100), Right(yv1100), gb, app(app(ty_@2, gd), ge)) → new_esEs0(yv100, yv1100, gd, ge)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), cb, app(ty_Maybe, cc)) → new_esEs(yv101, yv1101, cc)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), cb, app(app(ty_Either, cf), cg)) → new_esEs1(yv101, yv1101, cf, cg)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), app(app(ty_@2, dg), dh), df) → new_esEs0(yv100, yv1100, dg, dh)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), app(app(ty_Either, bcd), bce), he, bah) → new_esEs1(yv100, yv1100, bcd, bce)
new_esEs1(Right(yv100), Right(yv1100), gb, app(ty_Maybe, gc)) → new_esEs(yv100, yv1100, gc)
new_esEs0(@2(yv100, yv101), @2(yv1100, yv1101), cb, app(app(ty_@2, cd), ce)) → new_esEs0(yv101, yv1101, cd, ce)
new_esEs3(:(yv100, yv101), :(yv1100, yv1101), app(ty_Maybe, bdc)) → new_esEs(yv100, yv1100, bdc)
new_esEs2(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), hd, he, app(app(app(ty_@3, bac), bad), bae)) → new_esEs2(yv102, yv1102, bac, bad, bae)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe0(yv10, yv110, yv26, yv111, yv27, bb) → new_listToMaybe(yv26, new_esEs4(yv10, yv110, bb), yv10, yv111, yv27, bb)
new_listToMaybe(yv34, False, yv36, :(yv370, yv371), yv38, ba) → new_listToMaybe0(yv36, yv370, new_primPlusNat0(yv38, Zero), yv371, new_primPlusNat0(yv38, Zero), ba)

The TRS R consists of the following rules:

new_esEs4(yv10, yv110, app(app(app(ty_@3, baf), bag), bah)) → new_esEs14(yv10, yv110, baf, bag, bah)
new_esEs25(yv101, yv1101, ty_Char) → new_esEs19(yv101, yv1101)
new_esEs7(Just(yv100), Just(yv1100), app(ty_Maybe, bba)) → new_esEs7(yv100, yv1100, bba)
new_esEs21(yv100, yv1100, ty_@0) → new_esEs13(yv100, yv1100)
new_esEs7(Just(yv100), Just(yv1100), app(app(ty_Either, bbe), bbf)) → new_esEs12(yv100, yv1100, bbe, bbf)
new_esEs12(Right(yv100), Right(yv1100), hb, ty_@0) → new_esEs13(yv100, yv1100)
new_esEs20(yv101, yv1101, app(ty_Maybe, da)) → new_esEs7(yv101, yv1101, da)
new_primPlusNat1(Succ(yv5200), Succ(yv1101000)) → Succ(Succ(new_primPlusNat1(yv5200, yv1101000)))
new_primEqInt(Neg(Succ(yv1000)), Pos(yv1100)) → False
new_primEqInt(Pos(Succ(yv1000)), Neg(yv1100)) → False
new_esEs26(yv100, yv1100, app(app(ty_Either, bfc), bfd)) → new_esEs12(yv100, yv1100, bfc, bfd)
new_esEs7(Just(yv100), Nothing, bae) → False
new_esEs7(Nothing, Just(yv1100), bae) → False
new_esEs25(yv101, yv1101, ty_@0) → new_esEs13(yv101, yv1101)
new_esEs11(@2(yv100, yv101), @2(yv1100, yv1101), cf, cg) → new_asAs(new_esEs21(yv100, yv1100, cf), new_esEs20(yv101, yv1101, cg))
new_esEs12(Right(yv100), Right(yv1100), hb, ty_Integer) → new_esEs17(yv100, yv1100)
new_primEqInt(Neg(Zero), Pos(Succ(yv11000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yv11000))) → False
new_esEs6(yv100, yv1100, ty_Integer) → new_esEs17(yv100, yv1100)
new_esEs13(@0, @0) → True
new_esEs4(yv10, yv110, ty_Int) → new_esEs18(yv10, yv110)
new_esEs5([], [], bc) → True
new_esEs20(yv101, yv1101, ty_Bool) → new_esEs10(yv101, yv1101)
new_esEs23(yv100, yv1100, ty_Int) → new_esEs18(yv100, yv1100)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs4(yv10, yv110, ty_Double) → new_esEs15(yv10, yv110)
new_esEs20(yv101, yv1101, ty_Char) → new_esEs19(yv101, yv1101)
new_primMulNat0(Zero, Zero) → Zero
new_esEs24(yv102, yv1102, app(app(ty_Either, bcg), bch)) → new_esEs12(yv102, yv1102, bcg, bch)
new_esEs4(yv10, yv110, app(ty_Maybe, bae)) → new_esEs7(yv10, yv110, bae)
new_esEs25(yv101, yv1101, ty_Bool) → new_esEs10(yv101, yv1101)
new_esEs26(yv100, yv1100, ty_Float) → new_esEs16(yv100, yv1100)
new_esEs21(yv100, yv1100, app(app(app(ty_@3, fa), fb), fc)) → new_esEs14(yv100, yv1100, fa, fb, fc)
new_esEs5(:(yv100, yv101), :(yv1100, yv1101), bc) → new_asAs(new_esEs6(yv100, yv1100, bc), new_esEs5(yv101, yv1101, bc))
new_esEs21(yv100, yv1100, app(ty_[], fd)) → new_esEs5(yv100, yv1100, fd)
new_esEs24(yv102, yv1102, ty_@0) → new_esEs13(yv102, yv1102)
new_esEs12(Right(yv100), Right(yv1100), hb, app(app(ty_@2, he), hf)) → new_esEs11(yv100, yv1100, he, hf)
new_esEs12(Right(yv100), Right(yv1100), hb, ty_Int) → new_esEs18(yv100, yv1100)
new_esEs6(yv100, yv1100, ty_Ordering) → new_esEs8(yv100, yv1100)
new_esEs5([], :(yv1100, yv1101), bc) → False
new_esEs5(:(yv100, yv101), [], bc) → False
new_esEs4(yv10, yv110, ty_Ordering) → new_esEs8(yv10, yv110)
new_esEs7(Just(yv100), Just(yv1100), ty_Integer) → new_esEs17(yv100, yv1100)
new_esEs20(yv101, yv1101, app(app(ty_Either, de), df)) → new_esEs12(yv101, yv1101, de, df)
new_esEs21(yv100, yv1100, app(app(ty_Either, eg), eh)) → new_esEs12(yv100, yv1100, eg, eh)
new_primPlusNat0(Zero, yv110100) → Succ(yv110100)
new_esEs6(yv100, yv1100, ty_@0) → new_esEs13(yv100, yv1100)
new_esEs12(Right(yv100), Right(yv1100), hb, app(ty_Maybe, hc)) → new_esEs7(yv100, yv1100, hc)
new_esEs26(yv100, yv1100, ty_Int) → new_esEs18(yv100, yv1100)
new_esEs12(Left(yv100), Left(yv1100), ty_Double, fh) → new_esEs15(yv100, yv1100)
new_sr(Pos(yv1010), Neg(yv11010)) → Neg(new_primMulNat0(yv1010, yv11010))
new_sr(Neg(yv1010), Pos(yv11010)) → Neg(new_primMulNat0(yv1010, yv11010))
new_esEs7(Just(yv100), Just(yv1100), ty_Bool) → new_esEs10(yv100, yv1100)
new_esEs6(yv100, yv1100, ty_Int) → new_esEs18(yv100, yv1100)
new_esEs20(yv101, yv1101, ty_Int) → new_esEs18(yv101, yv1101)
new_esEs12(Left(yv100), Left(yv1100), ty_Char, fh) → new_esEs19(yv100, yv1100)
new_esEs12(Left(yv100), Right(yv1100), hb, fh) → False
new_esEs12(Right(yv100), Left(yv1100), hb, fh) → False
new_esEs24(yv102, yv1102, ty_Double) → new_esEs15(yv102, yv1102)
new_esEs25(yv101, yv1101, ty_Double) → new_esEs15(yv101, yv1101)
new_esEs21(yv100, yv1100, app(ty_Maybe, ec)) → new_esEs7(yv100, yv1100, ec)
new_esEs7(Just(yv100), Just(yv1100), ty_Char) → new_esEs19(yv100, yv1100)
new_esEs25(yv101, yv1101, ty_Integer) → new_esEs17(yv101, yv1101)
new_esEs12(Right(yv100), Right(yv1100), hb, ty_Float) → new_esEs16(yv100, yv1100)
new_esEs10(True, True) → True
new_esEs12(Right(yv100), Right(yv1100), hb, ty_Bool) → new_esEs10(yv100, yv1100)
new_esEs7(Just(yv100), Just(yv1100), app(ty_Ratio, bbb)) → new_esEs9(yv100, yv1100, bbb)
new_esEs6(yv100, yv1100, app(ty_Ratio, be)) → new_esEs9(yv100, yv1100, be)
new_esEs12(Left(yv100), Left(yv1100), app(app(ty_Either, gd), ge), fh) → new_esEs12(yv100, yv1100, gd, ge)
new_esEs12(Left(yv100), Left(yv1100), ty_Float, fh) → new_esEs16(yv100, yv1100)
new_primEqNat0(Zero, Succ(yv11000)) → False
new_primEqNat0(Succ(yv1000), Zero) → False
new_esEs17(Integer(yv100), Integer(yv1100)) → new_primEqInt(yv100, yv1100)
new_esEs4(yv10, yv110, app(ty_[], bc)) → new_esEs5(yv10, yv110, bc)
new_esEs12(Right(yv100), Right(yv1100), hb, app(ty_[], bad)) → new_esEs5(yv100, yv1100, bad)
new_esEs20(yv101, yv1101, app(ty_[], eb)) → new_esEs5(yv101, yv1101, eb)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs21(yv100, yv1100, app(app(ty_@2, ee), ef)) → new_esEs11(yv100, yv1100, ee, ef)
new_esEs26(yv100, yv1100, ty_Bool) → new_esEs10(yv100, yv1100)
new_esEs9(:%(yv100, yv101), :%(yv1100, yv1101), ff) → new_asAs(new_esEs23(yv100, yv1100, ff), new_esEs22(yv101, yv1101, ff))
new_esEs12(Left(yv100), Left(yv1100), ty_@0, fh) → new_esEs13(yv100, yv1100)
new_esEs12(Left(yv100), Left(yv1100), ty_Bool, fh) → new_esEs10(yv100, yv1100)
new_esEs26(yv100, yv1100, ty_@0) → new_esEs13(yv100, yv1100)
new_esEs24(yv102, yv1102, app(ty_Maybe, bcc)) → new_esEs7(yv102, yv1102, bcc)
new_esEs16(Float(yv100, yv101), Float(yv1100, yv1101)) → new_esEs18(new_sr(yv100, yv1100), new_sr(yv101, yv1101))
new_esEs21(yv100, yv1100, ty_Double) → new_esEs15(yv100, yv1100)
new_esEs4(yv10, yv110, ty_Char) → new_esEs19(yv10, yv110)
new_esEs21(yv100, yv1100, ty_Int) → new_esEs18(yv100, yv1100)
new_esEs6(yv100, yv1100, ty_Bool) → new_esEs10(yv100, yv1100)
new_esEs18(yv10, yv110) → new_primEqInt(yv10, yv110)
new_esEs20(yv101, yv1101, ty_Integer) → new_esEs17(yv101, yv1101)
new_esEs26(yv100, yv1100, ty_Char) → new_esEs19(yv100, yv1100)
new_esEs4(yv10, yv110, ty_@0) → new_esEs13(yv10, yv110)
new_esEs25(yv101, yv1101, app(ty_Maybe, bde)) → new_esEs7(yv101, yv1101, bde)
new_esEs19(Char(yv100), Char(yv1100)) → new_primEqNat0(yv100, yv1100)
new_esEs8(LT, LT) → True
new_esEs21(yv100, yv1100, ty_Integer) → new_esEs17(yv100, yv1100)
new_esEs12(Left(yv100), Left(yv1100), app(app(app(ty_@3, gf), gg), gh), fh) → new_esEs14(yv100, yv1100, gf, gg, gh)
new_esEs12(Right(yv100), Right(yv1100), hb, ty_Char) → new_esEs19(yv100, yv1100)
new_esEs25(yv101, yv1101, ty_Ordering) → new_esEs8(yv101, yv1101)
new_esEs12(Right(yv100), Right(yv1100), hb, ty_Ordering) → new_esEs8(yv100, yv1100)
new_sr(Neg(yv1010), Neg(yv11010)) → Pos(new_primMulNat0(yv1010, yv11010))
new_sr(Pos(yv1010), Pos(yv11010)) → Pos(new_primMulNat0(yv1010, yv11010))
new_asAs(False, yv51) → False
new_esEs25(yv101, yv1101, app(ty_[], bef)) → new_esEs5(yv101, yv1101, bef)
new_esEs25(yv101, yv1101, app(ty_Ratio, bdf)) → new_esEs9(yv101, yv1101, bdf)
new_esEs22(yv101, yv1101, ty_Int) → new_esEs18(yv101, yv1101)
new_primEqNat0(Zero, Zero) → True
new_esEs25(yv101, yv1101, app(app(ty_@2, bdg), bdh)) → new_esEs11(yv101, yv1101, bdg, bdh)
new_primMulNat0(Succ(yv10100), Zero) → Zero
new_primMulNat0(Zero, Succ(yv110100)) → Zero
new_esEs4(yv10, yv110, ty_Bool) → new_esEs10(yv10, yv110)
new_esEs21(yv100, yv1100, ty_Ordering) → new_esEs8(yv100, yv1100)
new_esEs12(Left(yv100), Left(yv1100), app(ty_Ratio, ga), fh) → new_esEs9(yv100, yv1100, ga)
new_esEs26(yv100, yv1100, app(ty_Maybe, beg)) → new_esEs7(yv100, yv1100, beg)
new_esEs20(yv101, yv1101, ty_Float) → new_esEs16(yv101, yv1101)
new_esEs7(Just(yv100), Just(yv1100), ty_@0) → new_esEs13(yv100, yv1100)
new_esEs12(Left(yv100), Left(yv1100), ty_Integer, fh) → new_esEs17(yv100, yv1100)
new_esEs26(yv100, yv1100, app(ty_Ratio, beh)) → new_esEs9(yv100, yv1100, beh)
new_esEs24(yv102, yv1102, ty_Integer) → new_esEs17(yv102, yv1102)
new_esEs4(yv10, yv110, ty_Integer) → new_esEs17(yv10, yv110)
new_esEs12(Left(yv100), Left(yv1100), app(app(ty_@2, gb), gc), fh) → new_esEs11(yv100, yv1100, gb, gc)
new_esEs26(yv100, yv1100, ty_Ordering) → new_esEs8(yv100, yv1100)
new_esEs24(yv102, yv1102, ty_Char) → new_esEs19(yv102, yv1102)
new_esEs24(yv102, yv1102, app(ty_[], bdd)) → new_esEs5(yv102, yv1102, bdd)
new_esEs8(GT, GT) → True
new_esEs15(Double(yv100, yv101), Double(yv1100, yv1101)) → new_esEs18(new_sr(yv100, yv1100), new_sr(yv101, yv1101))
new_esEs6(yv100, yv1100, ty_Float) → new_esEs16(yv100, yv1100)
new_primPlusNat0(Succ(yv520), yv110100) → Succ(Succ(new_primPlusNat1(yv520, yv110100)))
new_esEs26(yv100, yv1100, app(ty_[], bfh)) → new_esEs5(yv100, yv1100, bfh)
new_esEs12(Right(yv100), Right(yv1100), hb, app(app(app(ty_@3, baa), bab), bac)) → new_esEs14(yv100, yv1100, baa, bab, bac)
new_esEs25(yv101, yv1101, ty_Float) → new_esEs16(yv101, yv1101)
new_esEs20(yv101, yv1101, app(app(app(ty_@3, dg), dh), ea)) → new_esEs14(yv101, yv1101, dg, dh, ea)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs12(Left(yv100), Left(yv1100), app(ty_[], ha), fh) → new_esEs5(yv100, yv1100, ha)
new_esEs12(Left(yv100), Left(yv1100), ty_Int, fh) → new_esEs18(yv100, yv1100)
new_esEs4(yv10, yv110, app(app(ty_Either, hb), fh)) → new_esEs12(yv10, yv110, hb, fh)
new_primEqInt(Neg(Succ(yv1000)), Neg(Succ(yv11000))) → new_primEqNat0(yv1000, yv11000)
new_esEs6(yv100, yv1100, app(app(ty_@2, bf), bg)) → new_esEs11(yv100, yv1100, bf, bg)
new_esEs20(yv101, yv1101, ty_Ordering) → new_esEs8(yv101, yv1101)
new_esEs7(Just(yv100), Just(yv1100), ty_Int) → new_esEs18(yv100, yv1100)
new_primPlusNat1(Zero, Succ(yv1101000)) → Succ(yv1101000)
new_primPlusNat1(Succ(yv5200), Zero) → Succ(yv5200)
new_esEs7(Just(yv100), Just(yv1100), app(app(ty_@2, bbc), bbd)) → new_esEs11(yv100, yv1100, bbc, bbd)
new_esEs21(yv100, yv1100, app(ty_Ratio, ed)) → new_esEs9(yv100, yv1100, ed)
new_esEs12(Left(yv100), Left(yv1100), app(ty_Maybe, fg), fh) → new_esEs7(yv100, yv1100, fg)
new_esEs20(yv101, yv1101, app(ty_Ratio, db)) → new_esEs9(yv101, yv1101, db)
new_esEs12(Right(yv100), Right(yv1100), hb, ty_Double) → new_esEs15(yv100, yv1100)
new_esEs25(yv101, yv1101, ty_Int) → new_esEs18(yv101, yv1101)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs6(yv100, yv1100, ty_Double) → new_esEs15(yv100, yv1100)
new_esEs24(yv102, yv1102, ty_Bool) → new_esEs10(yv102, yv1102)
new_esEs4(yv10, yv110, ty_Float) → new_esEs16(yv10, yv110)
new_esEs7(Just(yv100), Just(yv1100), ty_Float) → new_esEs16(yv100, yv1100)
new_esEs7(Just(yv100), Just(yv1100), ty_Ordering) → new_esEs8(yv100, yv1100)
new_esEs12(Right(yv100), Right(yv1100), hb, app(app(ty_Either, hg), hh)) → new_esEs12(yv100, yv1100, hg, hh)
new_esEs25(yv101, yv1101, app(app(ty_Either, bea), beb)) → new_esEs12(yv101, yv1101, bea, beb)
new_esEs6(yv100, yv1100, ty_Char) → new_esEs19(yv100, yv1100)
new_esEs22(yv101, yv1101, ty_Integer) → new_esEs17(yv101, yv1101)
new_esEs7(Just(yv100), Just(yv1100), app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs14(yv100, yv1100, bbg, bbh, bca)
new_primEqInt(Neg(Zero), Neg(Succ(yv11000))) → False
new_primEqInt(Neg(Succ(yv1000)), Neg(Zero)) → False
new_esEs8(EQ, EQ) → True
new_esEs23(yv100, yv1100, ty_Integer) → new_esEs17(yv100, yv1100)
new_esEs10(False, False) → True
new_primPlusNat1(Zero, Zero) → Zero
new_esEs26(yv100, yv1100, app(app(app(ty_@3, bfe), bff), bfg)) → new_esEs14(yv100, yv1100, bfe, bff, bfg)
new_esEs12(Left(yv100), Left(yv1100), ty_Ordering, fh) → new_esEs8(yv100, yv1100)
new_esEs6(yv100, yv1100, app(ty_Maybe, bd)) → new_esEs7(yv100, yv1100, bd)
new_esEs24(yv102, yv1102, ty_Float) → new_esEs16(yv102, yv1102)
new_asAs(True, yv51) → yv51
new_esEs20(yv101, yv1101, ty_Double) → new_esEs15(yv101, yv1101)
new_primMulNat0(Succ(yv10100), Succ(yv110100)) → new_primPlusNat0(new_primMulNat0(yv10100, Succ(yv110100)), yv110100)
new_esEs24(yv102, yv1102, app(app(ty_@2, bce), bcf)) → new_esEs11(yv102, yv1102, bce, bcf)
new_esEs4(yv10, yv110, app(ty_Ratio, ff)) → new_esEs9(yv10, yv110, ff)
new_esEs6(yv100, yv1100, app(app(ty_Either, bh), ca)) → new_esEs12(yv100, yv1100, bh, ca)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs26(yv100, yv1100, ty_Double) → new_esEs15(yv100, yv1100)
new_esEs26(yv100, yv1100, ty_Integer) → new_esEs17(yv100, yv1100)
new_primEqInt(Pos(Succ(yv1000)), Pos(Succ(yv11000))) → new_primEqNat0(yv1000, yv11000)
new_esEs7(Just(yv100), Just(yv1100), ty_Double) → new_esEs15(yv100, yv1100)
new_esEs24(yv102, yv1102, ty_Int) → new_esEs18(yv102, yv1102)
new_esEs7(Just(yv100), Just(yv1100), app(ty_[], bcb)) → new_esEs5(yv100, yv1100, bcb)
new_primEqNat0(Succ(yv1000), Succ(yv11000)) → new_primEqNat0(yv1000, yv11000)
new_esEs20(yv101, yv1101, app(app(ty_@2, dc), dd)) → new_esEs11(yv101, yv1101, dc, dd)
new_esEs25(yv101, yv1101, app(app(app(ty_@3, bec), bed), bee)) → new_esEs14(yv101, yv1101, bec, bed, bee)
new_esEs6(yv100, yv1100, app(ty_[], ce)) → new_esEs5(yv100, yv1100, ce)
new_esEs21(yv100, yv1100, ty_Bool) → new_esEs10(yv100, yv1100)
new_esEs12(Right(yv100), Right(yv1100), hb, app(ty_Ratio, hd)) → new_esEs9(yv100, yv1100, hd)
new_esEs24(yv102, yv1102, ty_Ordering) → new_esEs8(yv102, yv1102)
new_esEs21(yv100, yv1100, ty_Float) → new_esEs16(yv100, yv1100)
new_esEs24(yv102, yv1102, app(ty_Ratio, bcd)) → new_esEs9(yv102, yv1102, bcd)
new_esEs20(yv101, yv1101, ty_@0) → new_esEs13(yv101, yv1101)
new_esEs7(Nothing, Nothing, bae) → True
new_esEs24(yv102, yv1102, app(app(app(ty_@3, bda), bdb), bdc)) → new_esEs14(yv102, yv1102, bda, bdb, bdc)
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(yv11000))) → False
new_primEqInt(Pos(Succ(yv1000)), Pos(Zero)) → False
new_esEs21(yv100, yv1100, ty_Char) → new_esEs19(yv100, yv1100)
new_esEs14(@3(yv100, yv101, yv102), @3(yv1100, yv1101, yv1102), baf, bag, bah) → new_asAs(new_esEs26(yv100, yv1100, baf), new_asAs(new_esEs25(yv101, yv1101, bag), new_esEs24(yv102, yv1102, bah)))
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs4(yv10, yv110, app(app(ty_@2, cf), cg)) → new_esEs11(yv10, yv110, cf, cg)
new_esEs6(yv100, yv1100, app(app(app(ty_@3, cb), cc), cd)) → new_esEs14(yv100, yv1100, cb, cc, cd)
new_esEs26(yv100, yv1100, app(app(ty_@2, bfa), bfb)) → new_esEs11(yv100, yv1100, bfa, bfb)

The set Q consists of the following terms:

new_esEs6(x0, x1, ty_Double)
new_esEs13(@0, @0)
new_esEs7(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs20(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Float)
new_esEs12(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs21(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs15(Double(x0, x1), Double(x2, x3))
new_esEs24(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs21(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Int)
new_esEs12(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs12(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs12(Left(x0), Right(x1), x2, x3)
new_esEs12(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_asAs(True, x0)
new_esEs21(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Ordering)
new_esEs8(EQ, EQ)
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs25(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Int)
new_esEs12(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, ty_Float)
new_esEs12(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs12(Right(x0), Right(x1), x2, ty_Bool)
new_esEs21(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Float)
new_esEs12(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs11(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs7(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Char)
new_esEs12(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs7(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs12(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(GT, GT)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs7(Just(x0), Just(x1), ty_Double)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs8(LT, LT)
new_esEs16(Float(x0, x1), Float(x2, x3))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs12(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs6(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs17(Integer(x0), Integer(x1))
new_esEs12(Right(x0), Right(x1), x2, ty_Int)
new_esEs8(EQ, GT)
new_esEs8(GT, EQ)
new_primPlusNat1(Zero, Succ(x0))
new_esEs7(Just(x0), Just(x1), ty_Float)
new_esEs24(x0, x1, ty_Bool)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs12(Right(x0), Right(x1), x2, ty_Double)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs12(Right(x0), Right(x1), x2, ty_Char)
new_esEs10(False, False)
new_esEs6(x0, x1, ty_Int)
new_esEs7(Just(x0), Nothing, x1)
new_esEs7(Just(x0), Just(x1), ty_@0)
new_esEs24(x0, x1, ty_Integer)
new_esEs7(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Char)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs24(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Float)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Double)
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs6(x0, x1, ty_Ordering)
new_sr(Pos(x0), Pos(x1))
new_primMulNat0(Zero, Zero)
new_esEs12(Left(x0), Left(x1), ty_Ordering, x2)
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Ordering)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs5([], [], x0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs7(Just(x0), Just(x1), ty_Char)
new_primPlusNat0(Succ(x0), x1)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs12(Left(x0), Left(x1), ty_Integer, x2)
new_esEs7(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Integer)
new_esEs14(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs12(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(x0, x1, ty_@0)
new_esEs7(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Bool)
new_asAs(False, x0)
new_esEs26(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Char)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs21(x0, x1, ty_Integer)
new_esEs7(Just(x0), Just(x1), ty_Integer)
new_esEs7(Just(x0), Just(x1), ty_Int)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs7(Nothing, Just(x0), x1)
new_esEs7(Just(x0), Just(x1), ty_Ordering)
new_esEs12(Right(x0), Right(x1), x2, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs12(Right(x0), Right(x1), x2, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Integer)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs6(x0, x1, ty_Float)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs20(x0, x1, ty_@0)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs12(Left(x0), Left(x1), ty_Int, x2)
new_esEs12(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primPlusNat0(Zero, x0)
new_esEs4(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Left(x0), Left(x1), ty_Float, x2)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Succ(x1))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primPlusNat1(Zero, Zero)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_@0)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_primMulNat0(Zero, Succ(x0))
new_esEs10(True, True)
new_esEs18(x0, x1)
new_esEs12(Left(x0), Left(x1), ty_Bool, x2)
new_esEs4(x0, x1, ty_Float)
new_esEs7(Nothing, Nothing, x0)
new_esEs9(:%(x0, x1), :%(x2, x3), x4)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primEqNat0(Succ(x0), Zero)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs12(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_@0)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs4(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs7(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Char)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5([], :(x0, x1), x2)
new_esEs20(x0, x1, app(ty_[], x2))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: